package de.rs.espresso.algorithms.tautology;

import de.rs.espresso.cubes.CubeFactory;
import de.rs.espresso.interfaces.ICover;
import de.rs.espresso.interfaces.ICube;
import de.rs.espresso.interfaces.IGlobalInformation;
import de.rs.espresso.tools.Statistics;

public class SimpleTautologyCheck {

	private enum SpecialCase {
		NONE, TAUTOLOGY, NO_TAUTOLOGY
	}

	private IGlobalInformation info;
	
	private int depth = 0;
	
	
	public SimpleTautologyCheck(IGlobalInformation info) {
		this.info = info;
	}

	/**
	 * 
	 * Checks if the given ICover is a tautology.
	 * 
	 * @param cover
	 * @param cube
	 * @return
	 */

	public boolean compute(ICover cover) {
		
		long measurementId = Statistics.startMeasurement("TAUTOLOGY");
		
		if(cover.isVoid()) {
			Statistics.stopMeasurement(measurementId);
			return false;
		}
			

		boolean result = recursiveTautologyCheck(cover);
		
		Statistics.stopMeasurement(measurementId);
		
		return result;

	}

	private boolean recursiveTautologyCheck(ICover cover) {
		
		depth++;

		// Check Special Cases:
		
		SpecialCase sc = specialCase(cover);

		if (sc.equals(SpecialCase.NO_TAUTOLOGY))
			return false;
		else if (sc.equals(SpecialCase.TAUTOLOGY))
			return true;

		// TODO: UNATE_REDUCTION, COMPONENT_REDUCTION

		
		
		//Binate Select:
		
		int literalPosition = cover.getMostBinateLiteral();
		
		ICube dcCube = CubeFactory.getDontCareCube(info);
		
		ICube splittingCubeLeft = dcCube.clone();
		splittingCubeLeft.setLiteral(literalPosition, ICube.DIRECT);
				
		ICube splittingCubeRight = dcCube;
		splittingCubeRight.setLiteral(literalPosition, ICube.NEGATED);
		
		
		//Recursive call:
		

		if (!recursiveTautologyCheck(cover
				.getCofactor(splittingCubeLeft)))
			return false;
		
		

		if (!recursiveTautologyCheck(cover
				.getCofactor(splittingCubeRight)))
			return false;
		

		return true;

	}

	private SpecialCase specialCase(ICover cover) {

		/*
		 * Check for row of Don't Cares.
		 */
		for (ICube cube : cover) {
			if (cube.isTautology())
				return SpecialCase.TAUTOLOGY;
		}
		
		if(cover.isUnate())
			return SpecialCase.NO_TAUTOLOGY;

		/*
		 * Equals the check, if there is a literal which only appears in one
		 * form: NEGATED or DIRECT form. (Book p. 65 Fig. 4.2.1 special case 2)
		 */
		
		assert(!cover.isEmpty()) : "Cover should not be empty at this point!";
		
		ICube andCube = cover.get(0).clone();
		ICube orCube = cover.get(0).clone();
		for (ICube cube : cover) {
			andCube = andCube.and(cube);
			orCube = orCube.or(cube);
		}

		int numberOfLiterals = info.getNumberOfInputs();

		for (int i = 0; i < numberOfLiterals; i++) {
			byte orLiteral = orCube.getLiteral(i);
			byte andLiteral = andCube.getLiteral(i);
			if (orLiteral==andLiteral&&orLiteral!=ICube.DONT_CARE)				
				return SpecialCase.NO_TAUTOLOGY;
		}

		/*
		 * (Book p. 65 Fig. 4.2.1 special case 3)
		 */
		if ((cover.getUpperBoundOfMinterms()) < (2 ^ numberOfLiterals))
			return SpecialCase.NO_TAUTOLOGY;

		// if(numberOfLiterals<8) {
		// //TODO: truth table , minterm test.
		// }

		return SpecialCase.NONE;
	}

}
